Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		0 + y	→ y
2:		s(x) + y	→ s(x + y)
3:		nil ++ ys	→ ys
4:		(x : xs) ++ ys	→ x : (xs ++ ys)
5:		sum(x : nil)	→ x : nil
6:		sum(x : (y : xs))	→ sum((x + y) : xs)
7:		sum(xs ++ (x : (y : ys)))	→ sum(xs ++ sum(x : (y : ys)))
8:		x - 0	→ x
9:		0 - s(y)	→ 0
10:		s(x) - s(y)	→ x - y
11:		quot(0,s(y))	→ 0
12:		quot(s(x),s(y))	→ s(quot(x - y,s(y)))
13:		length(nil)	→ 0
14:		length(x : xs)	→ s(length(xs))
15:		hd(x : xs)	→ x
16:		avg(xs)	→ quot(hd(sum(xs)),length(xs))

There are 15 dependency pairs:


17:		s(x) +# y	→ x +# y
18:		(x : xs) ++# ys	→ xs ++# ys
19:		SUM(x : (y : xs))	→ SUM((x + y) : xs)
20:		SUM(x : (y : xs))	→ x +# y
21:		SUM(xs ++ (x : (y : ys)))	→ SUM(xs ++ sum(x : (y : ys)))
22:		SUM(xs ++ (x : (y : ys)))	→ xs ++# sum(x : (y : ys))
23:		SUM(xs ++ (x : (y : ys)))	→ SUM(x : (y : ys))
24:		s(x) -# s(y)	→ x -# y
25:		QUOT(s(x),s(y))	→ QUOT(x - y,s(y))
26:		QUOT(s(x),s(y))	→ x -# y
27:		LENGTH(x : xs)	→ LENGTH(xs)
28:		AVG(xs)	→ QUOT(hd(sum(xs)),length(xs))
29:		AVG(xs)	→ HD(sum(xs))
30:		AVG(xs)	→ SUM(xs)
31:		AVG(xs)	→ LENGTH(xs)

The approximated dependency graph contains 7 SCCs: {17}, {18}, {24}, {27}, {25}, {19} and {21}.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(+#) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {18}. There are no usable rules. By taking the AF π with π(++#) = 1 and π(:) = [2] together with the lexicographic path order with empty precedence, rule 18 is strictly decreasing.

Consider the SCC {24}. There are no usable rules. By taking the AF π with π(-#) = 1 together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.

Consider the SCC {27}. There are no usable rules. By taking the AF π with π(LENGTH) = 1 and π(:) = [2] together with the lexicographic path order with empty precedence, rule 27 is strictly decreasing.

Consider the SCC {25}. The usable rules are {8-10}. By taking the AF π with π(-) = π(QUOT) = 1 together with the lexicographic path order with empty precedence, the rules in {8,9} are weakly decreasing and the rules in {10,25} are strictly decreasing.

Consider the SCC {19}. The usable rules are {1,2}. By taking the AF π with π(s) = π(SUM) = 1, π(+) = 2 and π(:) = [2] together with the lexicographic path order with empty precedence, the rules in {1,2} are weakly decreasing and rule 19 is strictly decreasing.

Consider the SCC {21}. The usable rules are {1-7}. The constraints could not be solved.

Tyrolean Termination Tool (0.19 seconds) --- May 4, 2006